10/15/2008 Lesson Plan

- Finish slides on symmetry breaking 

First order logic

What are the elements of FOL?

Predicates
Terms
Constants
Functors
Quantifiers

Looks a lot like propositional schema.  How does it differ?
Several important ways:

* The notion of a "possible world" is enriched to include not just propositions, but 
  also individuals, relationships, and functions.  Where W is a possible world,

W: Sentences --> { true, false }  (just like propositional logic)
W: Propositions --> { true, false } (just like propositional logic)
W: Constants --> Individuals 
W: Functor --> Functions from (Individuals^K --> Individuals)
W: Terms --> Individuals
W: Predicates --> Relationships over Individuals

The set of Individuals may be *infinite*.  It may be *larger* than the set of
constants.  Functors can be used to generate an infinite number of names (terms):

E.g.: the natural numbers:  0 (constant), s(0) (successor of 0), s(s(0)), s(s(s(0))),...

If we have an infinite number of terms, with even one predicate we can generate an
infinite number of propositions, eg:

Positive(s(0)),  Positive(s(s(0))),  Positive(s(s(s(0)))), ...

In summary: 
Propositional logic can only talk about FINITE domains.
FOL can talk about finite or INFINITE domains.

* Another difference: Quantification is defined over the (possible infinite) domain
  of a model, NOT just over the constants in the formula.  In fact, quantification is
  not even limited to the TERMS in the formula -- you can have worlds where some
  individuals do not have a name!

  For example:
  
  {car(ford) & car(chevy) & ugly(ford) & ugly(chevy) }  |=/=  A x . car(x) => ugly(x)

Why not?  Because the sentence on the left can be true in worlds where there are
other cars that are not ugly!  For example, a world M where
    M(car) = { *ford*, *chevy*, *toyota* }
    M(ugly) = { *ford*, *chevy* }

* When using propositional schema, we assumed that the different constants named
different individuals.  However, in FOL two different terms might refer to the SAME
individual in a model.  For example, the sentence above has a model where

    M(car) = { *ford* }
    M(ford) = { *ford* }
    M(chevy) = { *ford* }

This model is probably NOT one we intended to allow!  In order to be able to assert
which terms must be or cannot be the same individual, FOL uses a special predicate,
"=" equality.

In every world, equality is the reflective relationship over all the individuals in
that world.  So if M is world where Domain(M) = {  *ford*, *chevy*, *toyota* }, then

    M(=) = { (*ford*,*ford*), (*chevy*,*chevy*), (*toyota*,*toyota*) }

So lets write down the sentence that asserts that cars are either ford or chevy, and
both are ugly:

    car(ford) & car(chevy) & ugly(ford) & ugly(chevy) &
    ford =/= chevy & (A x . car(x) => (x=ford v x=chevy))

* Here is another way classical FOL is different from propositional schema.  In PS,
  functions such as "PLUS" were real implementated programming language functions that
  were executed when a schema was expanded.  Once the schema was turned into CNF,
  they were gone!

  By contrast, functors in FOL are just symbols used to construct TERMS.  If you use
  PLUS as the name of a functor, there is nothing that automatically makes it "mean"
  the addition operator, unless you WRITE AXIOMS THAT MAKE IT SO.  For example,

       A x,y . PLUS(0,y)=y
       A x,y . PLUS(s(x),y)=PLUS(x,s(y))

  Using these axioms you can PROVE, for example, that 
       PLUS(s(s(0)),s(0)) = s(s(s(0)))

  Phew!  This seems like an inefficient way to do arithmetic!  And who wants to use
  s(s(s(0))) to write "3"?  You can, in fact, have both the GENERALITY of FOL and the
  SIMPLICITY of PS, by extending FOL with the "syntactic sugar" of real functions
  that are evaluated BEFORE a formula goes to a theorem prover.  This is called
  "semantic attachment", and we'll see examples of it later.

  Here are some good uses for functions:

  - to create an infinite set of terms: e.g., 0, s(0), s(s(0)), ...

  - to specify many to one relationships: e.g.,
        father(x)  -- the individual who is the father of x
        A x . human(x) => human(father(x))
        A x,y . child(x,y) => y=father(x)

  - to create complex data structures.  For example:
    Suppose we want to reason about LISTS.  We can create a functor, lets call it 
    "cons", that maps a individual and a list to a new list:

    List(NIL)    
    A x,y . List(y) => List(cons(x,y))

    Now we can define a predicate "car" that relates a list to its
    first element:

    A x,y . List(y) = Car(x, cons(x, y))

    Car(NIL, NIL)

----------
Discuss Eligibility for Citizenship example
----------
Next class: INFERENCE in FOL